SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Communicating sequential processes</title>

</head>

Communicating sequential processes

</h1>

</header>

In <a href="Computer_science" title="Computer science">computer science</a>, communicating sequential processes (CSP) is a <a href="Formal_language" title="Formal language">formal language</a> for describing <a href="Pattern" title="Pattern">patterns</a> of interaction in <a href="Concurrent_systems" class="mw-redirect" title="Concurrent systems">concurrent systems</a>.<a href="#cite_note-roscoe-1">[1]</a> It is a member of the family of mathematical theories of concurrency known as process algebras, or <a href="Process_calculus" title="Process calculus">process calculi</a>, based on <a href="Message_passing" title="Message passing">message passing</a> via <a href="Channel_(programming)" title="Channel (programming)">channels</a>. CSP was highly influential in the design of the <a href="Occam_(programming_language)" title="Occam (programming language)">occam</a> programming language<a href="#cite_note-roscoe-1">[1]</a><a href="#cite_note-2">[2]</a> and also influenced the design of programming languages such as <a href="Limbo_(programming_language)" title="Limbo (programming language)">Limbo</a>,<a href="#cite_note-cox-3">[3]</a> <a href="RaftLib" title="RaftLib">RaftLib</a>, <a href="Erlang_(programming_language)" title="Erlang (programming language)">Erlang</a>,<a href="#cite_note-4">[4]</a> <a href="Go_(programming_language)" title="Go (programming language)">Go</a>,<a href="#cite_note-golang-5">[5]</a><a href="#cite_note-cox-3">[3]</a> <a href="Crystal_(programming_language)" title="Crystal (programming language)">Crystal</a>, and <a href="Clojure" title="Clojure">Clojure</a>'s core.async.<a href="#cite_note-clojure-core-async-6">[6]</a>

CSP was first described by <a href="Tony_Hoare" title="Tony Hoare">Tony Hoare</a> in a 1978 article,<a href="#cite_note-hoare1978-7">[7]</a> and has since evolved substantially.<a href="#cite_note-25years-8">[8]</a> CSP has been practically applied in industry as a tool for <a href="Formal_specification" title="Formal specification">specifying and verifying</a> the concurrent aspects of a variety of different systems, such as the T9000 <a href="Transputer" title="Transputer">Transputer</a>,<a href="#cite_note-barrett-9">[9]</a> as well as a secure <a href="E-commerce" title="E-commerce">e-commerce</a> system.<a href="#cite_note-hall-10">[10]</a> The theory of CSP itself is also still the subject of active research, including work to increase its range of practical applicability (e.g., increasing the scale of the systems that can be tractably analyzed).<a href="#cite_note-11">[11]</a>

<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Original_version">Original version</h3></div>

The version of CSP presented in Hoare's original 1978 article was essentially a concurrent programming language rather than a <a href="Process_calculus" title="Process calculus">process calculus</a>. It had a substantially different <a href="Syntax" title="Syntax">syntax</a> than later versions of CSP, did not possess mathematically defined semantics,<a href="#cite_note-hoare-12">[12]</a> and was unable to represent <a href="Unbounded_nondeterminism" title="Unbounded nondeterminism">unbounded nondeterminism</a>.<a href="#cite_note-clinger1981-13">[13]</a> Programs in the original CSP were written as a parallel composition of a fixed number of sequential processes communicating with each other strictly through synchronous message-passing. In contrast to later versions of CSP, each process was assigned an explicit name, and the source or destination of a message was defined by specifying the name of the intended sending or receiving process. For example, the process

<pre>COPY = *[c:character; west?c → east!c]

</pre>

repeatedly receives a character from the process named <code>west</code> and sends that character to process named <code>east</code>. The parallel composition

<pre>[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

</pre>

assigns the names <code>west</code> to the <code>DISASSEMBLE</code> process, <code>X</code> to the <code>COPY</code> process, and <code>east</code> to the <code>ASSEMBLE</code> process, and executes these three processes concurrently.<a href="#cite_note-hoare1978-7">[7]</a>

<div class="mw-heading mw-heading3"><h3 id="Development_into_process_algebra">Development into process algebra</h3></div>

Following the publication of the original version of CSP, Hoare, Stephen Brookes, and <a href="Bill_Roscoe" title="Bill Roscoe">A. W. Roscoe</a> developed and refined the theory of CSP into its modern, process algebraic form. The approach taken in developing CSP into a process algebra was influenced by <a href="Robin_Milner" title="Robin Milner">Robin Milner</a>'s work on the <a href="Calculus_of_Communicating_Systems" class="mw-redirect" title="Calculus of Communicating Systems">Calculus of Communicating Systems</a> (CCS) and conversely. The theoretical version of CSP was initially presented in a 1984 article by Brookes, Hoare, and Roscoe,<a href="#cite_note-14">[14]</a> and later in Hoare's book Communicating Sequential Processes,<a href="#cite_note-hoare-12">[12]</a> which was published in 1985. In September 2006, that book was still the <a rel="nofollow" class="external text" href="http://citeseer.ist.psu.edu/articles.html">third-most cited</a> <a href="Computer_science" title="Computer science">computer science</a> reference of all time according to <a href="Citeseer" class="mw-redirect" title="Citeseer">Citeseer</a> (albeit an unreliable source due to the nature of its sampling). The theory of CSP has undergone a few minor changes since the publication of Hoare's book. Most of these changes were motivated by the advent of automated tools for CSP process analysis and verification. Roscoe's The Theory and Practice of Concurrency<a href="#cite_note-roscoe-1">[1]</a> describes this newer version of CSP.

<div class="mw-heading mw-heading3"><h3 id="Applications">Applications</h3></div>

An early and important application of CSP was its use for specification and verification of elements of the INMOS T9000 <a href="Transputer" title="Transputer">Transputer</a>, a complex superscalar pipelined processor designed to support large-scale multiprocessing. CSP was employed in verifying the correctness of both the processor pipeline and the Virtual Channel Processor, which managed off-chip communications for the processor.<a href="#cite_note-barrett-9">[9]</a>

Industrial application of CSP to software design has usually focused on dependable and safety-critical systems. For example, the Bremen Institute for Safe Systems and <a href="DaimlerChrysler_Aerospace" class="mw-redirect" title="DaimlerChrysler Aerospace">Daimler-Benz Aerospace</a> modeled a fault-management system and avionics interface (consisting of about 23,000 lines of code) intended for use on the International Space Station in CSP, and analyzed the model to confirm that their design was free of <a href="Deadlock_(computer_science)" title="Deadlock (computer science)">deadlock</a> and <a href="Livelock" class="mw-redirect" title="Livelock">livelock</a>.<a href="#cite_note-15">[15]</a><a href="#cite_note-16">[16]</a> The modeling and analysis process was able to uncover a number of errors that would have been difficult to detect using testing alone. Similarly, <a href="Praxis_High_Integrity_Systems" class="mw-redirect" title="Praxis High Integrity Systems">Praxis High Integrity Systems</a> applied CSP modeling and analysis during the development of software (approximately 100,000 lines of code) for a secure smart-card certification authority to verify that their design was secure and free of deadlock. Praxis claims that the system has a much lower defect rate than comparable systems.<a href="#cite_note-hall-10">[10]</a>

Since CSP is well-suited to modeling and analyzing systems that incorporate complex message exchanges, it has also been applied to the verification of communications and security protocols. A prominent example of this sort of application is Lowe's use of CSP and the <a href="FDR2" class="mw-redirect" title="FDR2">FDR refinement-checker</a> to discover a previously unknown attack on the <a href="Needham%E2%80%93Schroeder_protocol" title="Needham–Schroeder protocol">Needham–Schroeder public-key authentication protocol</a>, and then to develop a corrected protocol able to defeat the attack.<a href="#cite_note-17">[17]</a>

<div class="mw-heading mw-heading2"><h2 id="Informal_description">Informal description</h2></div>

As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely through <a href="Message_passing" title="Message passing">message-passing</a> communication. However, the "Sequential" part of the CSP name is now something of a misnomer, since modern CSP allows component processes to be defined both as sequential processes, and as the parallel composition of more primitive processes. The relationships between different processes, and the way each process communicates with its environment, are described using various <a href="Process_calculi" class="mw-redirect" title="Process calculi">process algebraic</a> operators. Using this algebraic approach, quite complex process descriptions can be easily constructed from a few primitive elements.

<div class="mw-heading mw-heading3"><h3 id="Primitives">Primitives</h3></div>

CSP provides two classes of primitives in its process algebra: events and primitive processes.

<dl><dt>Events</dt></dl>

Events represent communications or interactions. They are assumed to be instantaneous, and their communication is all that an external ‘environment’ can know about processes. An event is communicated only if the environment allows it. If a process does offer an event and the environment allows it, then that event must be communicated. Events may be atomic names (e.g. on, off), compound names (e.g. valve.open, valve.close), or input/output events (e.g. mouse?xy, screen!bitmap). The set of all events is denoted <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>

</semantics>

</math><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy">.<a href="#cite_note-ucs-18">[18]</a>

<dl><dt>Primitive processes</dt></dl>

Primitive processes represent fundamental behaviors: examples include <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {STOP} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {STOP} }</annotation>

</semantics>

</math><img src="./e23c64a51333169346990cba6313d7d089153428.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.362ex; height:2.176ex;" alt="{\displaystyle \mathrm {STOP} }" loading="lazy"> (the process that immediately deadlocks), and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {SKIP} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {SKIP} }</annotation>

</semantics>

</math><img src="./a1e9539e2d302a05656375b16f38192cf5eeb11f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.523ex; height:2.176ex;" alt="{\displaystyle \mathrm {SKIP} }" loading="lazy"> (the process that immediately terminates successfully).<a href="#cite_note-ucs-18">[18]</a>

<div class="mw-heading mw-heading3"><h3 id="Algebraic_operators">Algebraic operators</h3></div>

CSP has a wide range of algebraic operators. The principal ones are informally given as follows.

<dl><dt>Prefix</dt></dl>

The prefix operator combines an event and a process to produce a new process. For example, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a\to P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a\to P}</annotation>

</semantics>

</math><img src="./133b76d8df4af3950a3007361949b0d8495e0ae1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.589ex; height:2.176ex;" alt="{\displaystyle a\to P}" loading="lazy"> is the process that is willing to communicate event <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a}</annotation>

</semantics>

</math><img src="./ffd2487510aa438433a2579450ab2b3d557e5edc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}" loading="lazy"> with its environment and, after <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a}</annotation>

</semantics>

</math><img src="./ffd2487510aa438433a2579450ab2b3d557e5edc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}" loading="lazy">, behaves like the process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">.<a href="#cite_note-ucs-18">[18]</a>

<dl><dt>Recursion</dt></dl>

Processes can be defined using recursion. Where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F(P)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F(P)}</annotation>

</semantics>

</math><img src="./9a17c476c3be3fb5250ad3b434c61ce44f5a8c56.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.296ex; height:2.843ex;" alt="{\displaystyle F(P)}" loading="lazy"> is any CSP term involving <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">, the process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mu P.F(P)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mu P.F(P)}</annotation>

</semantics>

</math><img src="./49776fc7d68f9cdd5c5e1abffee6ebe487548221.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.477ex; height:2.843ex;" alt="{\displaystyle \mu P.F(P)}" loading="lazy"> defines a recursive process given by the equation

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P=F(P)}</annotation>

</semantics>

</math><img src="./c6ece554738c73df6f29f6b9ae7fd4e9a3b767d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.139ex; height:2.843ex;" alt="{\displaystyle P=F(P)}" loading="lazy">.

Recursions can also be defined mutually, such as

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}&P_{u}=up\to P_{d}\\&P_{d}=down\to P_{u}\\\end{aligned}}}</annotation>

</semantics>

</math>

which defines a pair of mutually recursive processes that alternate between communicating <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle up}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle up}</annotation>

</semantics>

</math><img src="./06ec49923fc1d95927dbb0860e655dbeadd96be7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.499ex; height:2.009ex;" alt="{\displaystyle up}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle down}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle down}</annotation>

</semantics>

</math><img src="./64cac5ac5be04c6db85b8600681f58b9dad8df4a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.402ex; height:2.176ex;" alt="{\displaystyle down}" loading="lazy">.<a href="#cite_note-ucs-18">[18]</a>

<dl><dt>Deterministic choice</dt></dl>

The deterministic (or external) choice operator allows the future evolution of a process to be defined as a choice between two component processes and allows the environment to resolve the choice by communicating an initial event for one of the processes. For example, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (a\to P)\ \Box \ (b\to Q)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (a\to P)\ \Box \ (b\to Q)}</annotation>

</semantics>

</math><img src="./1887d94d53dde3de0a473f1523a522e3aecd59a8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.627ex; height:2.843ex;" alt="{\displaystyle (a\to P)\ \Box \ (b\to Q)}" loading="lazy"> is the process that is willing to communicate the initial events <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a}</annotation>

</semantics>

</math><img src="./ffd2487510aa438433a2579450ab2b3d557e5edc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle b}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle b}</annotation>

</semantics>

</math><img src="./f11423fbb2e967f986e36804a8ae4271734917c3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.998ex; height:2.176ex;" alt="{\displaystyle b}" loading="lazy"> and subsequently behaves as either <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> or <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy">, depending on which initial event the environment chooses to communicate.<a href="#cite_note-ucs-18">[18]</a>

<dl><dt>Nondeterministic choice</dt></dl>

The nondeterministic (or internal) choice operator allows the future evolution of a process to be defined as a choice between two component processes, but does not allow the environment any control over which one of the component processes will be selected. For example, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (a\to P)\sqcap (b\to Q)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (a\to P)\sqcap (b\to Q)}</annotation>

</semantics>

</math><img src="./95414a350ca4640a87fbd0e6b8feec1590ccee74.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.24ex; height:2.843ex;" alt="{\displaystyle (a\to P)\sqcap (b\to Q)}" loading="lazy"> can behave like either <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a\to P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a\to P}</annotation>

</semantics>

</math><img src="./133b76d8df4af3950a3007361949b0d8495e0ae1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.589ex; height:2.176ex;" alt="{\displaystyle a\to P}" loading="lazy"> or <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle b\to Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle b\to Q}</annotation>

</semantics>

</math><img src="./5347ef6c4e0472a27bba7bd69fa134ca1c86a9bd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.45ex; height:2.509ex;" alt="{\displaystyle b\to Q}" loading="lazy">. It can refuse to accept <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a}</annotation>

</semantics>

</math><img src="./ffd2487510aa438433a2579450ab2b3d557e5edc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}" loading="lazy"> or <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle b}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle b}</annotation>

</semantics>

</math><img src="./f11423fbb2e967f986e36804a8ae4271734917c3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.998ex; height:2.176ex;" alt="{\displaystyle b}" loading="lazy"> and is only obliged to communicate if the environment offers both <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a}</annotation>

</semantics>

</math><img src="./ffd2487510aa438433a2579450ab2b3d557e5edc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle b}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle b}</annotation>

</semantics>

</math><img src="./f11423fbb2e967f986e36804a8ae4271734917c3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.998ex; height:2.176ex;" alt="{\displaystyle b}" loading="lazy">.

Nondeterminism can be inadvertently introduced into an ostensibly deterministic choice if the initial events of both sides of the choice are identical. So, for example,

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (a\to a\to \mathrm {STOP} )\ \Box \ (a\to b\to \mathrm {STOP} )}</annotation>

</semantics>

</math> and

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a\to {\big (}(a\to \mathrm {STOP} )\sqcap (b\to \mathrm {STOP} ){\big )}}</annotation>

</semantics>

</math>

are equivalent.<a href="#cite_note-ucs-18">[18]</a>

<dl><dt>Interleaving</dt></dl>

The interleaving operator represents completely independent concurrent activity. The process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\;|||\;Q}">

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\;|||\;Q}</annotation>

</semantics>

</math><img src="./fb84e1dc95bffa6de0be618cb05da06fb57eb048.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.815ex; height:2.843ex;" alt="{\displaystyle P\;|||\;Q}" loading="lazy"> behaves as both <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> simultaneously. The events from both processes are arbitrarily interleaved in time. Interleaving can introduce nondeterminism even if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> are both deterministic: if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> can both communicate the same event, then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\;|||\;Q}">

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\;|||\;Q}</annotation>

</semantics>

</math><img src="./fb84e1dc95bffa6de0be618cb05da06fb57eb048.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.815ex; height:2.843ex;" alt="{\displaystyle P\;|||\;Q}" loading="lazy"> nondeterministically chooses which of the two processes communicated that event.<a href="#cite_note-ucs-18">[18]</a>

<dl><dt>Interface parallel</dt></dl>

The interface parallel (or generalized parallel) operator represents concurrent activity that requires synchronization between the component processes: for <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\;|[X]|\;Q}">

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\;|[X]|\;Q}</annotation>

</semantics>

</math><img src="./3a169a17eac57ea0b076b9c5daad4b158f4c581a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.441ex; height:2.843ex;" alt="{\displaystyle P\;|[X]|\;Q}" loading="lazy">, any event in the interface set <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle X\subseteq \Sigma }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle X\subseteq \Sigma }</annotation>

</semantics>

</math><img src="./18f79703984f68d0b2044ae1309747ac56db6702.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.757ex; height:2.343ex;" alt="{\displaystyle X\subseteq \Sigma }" loading="lazy"> can only occur when both <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> are able to engage in that event.<a href="#cite_note-ucs-18">[18]</a>

For example, the process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\;|[\{a\}]|\;Q}">

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\;|[\{a\}]|\;Q}</annotation>

</semantics>

</math><img src="./1110add2d6887cc858078505464de38be69440af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.016ex; height:2.843ex;" alt="{\displaystyle P\;|[\{a\}]|\;Q}" loading="lazy"> requires that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> must both be able to perform event <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a}</annotation>

</semantics>

</math><img src="./ffd2487510aa438433a2579450ab2b3d557e5edc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}" loading="lazy"> before that event can occur. So, the process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}">

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}</annotation>

</semantics>

</math><img src="./2f5452c43076d3766230220df36622759666e020.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.323ex; height:2.843ex;" alt="{\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}" loading="lazy"> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a\to (P\;|[\{a\}]|\;Q)}">

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a\to (P\;|[\{a\}]|\;Q)}</annotation>

</semantics>

</math><img src="./0a93248360edcfc6e819d305f1e736a29650764c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.669ex; height:2.843ex;" alt="{\displaystyle a\to (P\;|[\{a\}]|\;Q)}" loading="lazy">, while <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}">

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}</annotation>

</semantics>

</math><img src="./f9df56258eeb3810ac921769b698d753a0d7a0a5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:26.122ex; height:2.843ex;" alt="{\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}" loading="lazy"> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {STOP} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {STOP} }</annotation>

</semantics>

</math><img src="./e23c64a51333169346990cba6313d7d089153428.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.362ex; height:2.176ex;" alt="{\displaystyle \mathrm {STOP} }" loading="lazy"> (i.e. the process deadlocks).

<dl><dt>Hiding</dt></dl>

The hiding operator provides a way to abstract processes by making some events unobservable by the environment. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\setminus X}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\setminus X}</annotation>

</semantics>

</math><img src="./02bf2ddf24f8d7e68dc3b2cf4a326cfdcf3fc4f8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.92ex; height:2.843ex;" alt="{\displaystyle P\setminus X}" loading="lazy"> is the process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> with the event set <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle X}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle X}</annotation>

</semantics>

</math><img src="./68baa052181f707c662844a465bfeeb135e82bab.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.98ex; height:2.176ex;" alt="{\displaystyle X}" loading="lazy"> hidden.

A trivial example of hiding is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (a\to P)\setminus \{a\}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (a\to P)\setminus \{a\}}</annotation>

</semantics>

</math><img src="./f1a76233787cfefaba8630a212c2d355c5ceffa2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.148ex; height:2.843ex;" alt="{\displaystyle (a\to P)\setminus \{a\}}" loading="lazy"> which, assuming that the event <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle a}</annotation>

</semantics>

</math><img src="./ffd2487510aa438433a2579450ab2b3d557e5edc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}" loading="lazy"> doesn't appear in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">, simply reduces to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">. Hidden events are internalized as τ actions, which are invisible to and uncontrollable by the environment. The existence of hiding introduces an additional behaviour called <a href="Divergence_(computer_science)" title="Divergence (computer science)">divergence</a>, where an infinite sequence of τ actions is performed. This is captured by the process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathbf {div} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathbf {div} }</annotation>

</semantics>

</math><img src="./bb2fff6cac65ff8a19acf86ceaeba9b44abab48b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.638ex; height:2.176ex;" alt="{\displaystyle \mathbf {div} }" loading="lazy">, whose behaviour is solely to perform τ actions forever.<a href="#cite_note-ucs-18">[18]</a> For example, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\mu P.a\to P)\setminus \{a\}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\mu P.a\to P)\setminus \{a\}}</annotation>

</semantics>

</math><img src="./3d11e4752906bb52cc5ca135d5340a54d7e9d416.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.329ex; height:2.843ex;" alt="{\displaystyle (\mu P.a\to P)\setminus \{a\}}" loading="lazy"> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathbf {div} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathbf {div} }</annotation>

</semantics>

</math><img src="./bb2fff6cac65ff8a19acf86ceaeba9b44abab48b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.638ex; height:2.176ex;" alt="{\displaystyle \mathbf {div} }" loading="lazy">.

<div class="mw-heading mw-heading3"><h3 id="Examples">Examples</h3></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

One of the archetypal CSP examples is an abstract representation of a chocolate vending machine and its interactions with a person wishing to buy some chocolate. This vending machine might be able to carry out two different events, “coin” and “choc” which represent the insertion of payment and the delivery of a chocolate respectively. A machine which demands payment (only in cash) before offering a chocolate can be written as:

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {VendingMachine} =\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }</annotation>

</semantics>

</math>

A person who might choose to use a coin or card to make payments could be modelled as:

</mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {Person} =(\mathrm {coin} \rightarrow \mathrm {STOP} )\;\Box \;(\mathrm {card} \rightarrow \mathrm {STOP} )}</annotation>

</semantics>

</math>

These two processes can be put in parallel, so that they can interact with each other. The behaviour of the composite process depends on the events that the two component processes must synchronise on. Thus,

</mrow>

<mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }</annotation>

</semantics>

</math>

whereas if synchronization was only required on “coin”, we would obtain

</mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)}</annotation>

</semantics>

</math>

If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

<mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}}</annotation>

</semantics>

</math>

we get the nondeterministic process

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP} }</annotation>

</semantics>

</math>

This is a process which either offers a “choc” event and then stops, or just stops. In other words, if we treat the abstraction as an external view of the system (e.g., someone who does not see the decision reached by the person), <a href="Nondeterministic_algorithm" title="Nondeterministic algorithm">nondeterminism</a> has been introduced.

<div class="mw-heading mw-heading2"><h2 id="Formal_definition">Formal definition</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Syntax">Syntax</h3></div>

The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let e be an event, b be a boolean and X be a set of events. Then the basic <a href="Syntax" title="Syntax">syntax</a> of CSP can be defined as:

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mtd>

<mtd>

<mtext>prefixing</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>external</mtext>

</mrow>

<mtext>choice</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>nondeterministic</mtext>

</mrow>

<mtext>choice</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>interleaving</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>interface</mtext>

</mrow>

<mtext>parallel</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mtd>

<mtd>

<mtext>hiding</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>sequential</mtext>

</mrow>

<mtext>composition</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>boolean</mtext>

</mrow>

<mtext>conditional</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>timeout</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

<mtd>

<mtext>interrupt</mtext>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lcll}{Proc}&::=&\mathrm {STOP} &\;\\&|&\mathrm {SKIP} &\;\\&|&e\rightarrow {Proc}&({\text{prefixing}})\\&|&{Proc}\;\Box \;{Proc}&({\text{external}}\;{\text{choice}})\\&|&{Proc}\;\sqcap \;{Proc}&({\text{nondeterministic}}\;{\text{choice}})\\&|&{Proc}\;\vert \vert \vert \;{Proc}&({\text{interleaving}})\\&|&{Proc}\;|[\{X\}]|\;{Proc}&({\text{interface}}\;{\text{parallel}})\\&|&{Proc}\setminus X&({\text{hiding}})\\&|&{Proc};{Proc}&({\text{sequential}}\;{\text{composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{Proc}\;\mathrm {else} \;Proc&({\text{boolean}}\;{\text{conditional}})\\&|&{Proc}\;\triangleright \;{Proc}&({\text{timeout}})\\&|&{Proc}\;\triangle \;{Proc}&({\text{interrupt}})\end{array}}}</annotation>

</semantics>

</math>

Note that, in the interests of brevity, the syntax presented above omits the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathbf {div} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathbf {div} }</annotation>

</semantics>

</math><img src="./bb2fff6cac65ff8a19acf86ceaeba9b44abab48b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.638ex; height:2.176ex;" alt="{\displaystyle \mathbf {div} }" loading="lazy"> process, which represents <a href="Divergence_(computer_science)" title="Divergence (computer science)">divergence</a>, as well as various operators such as alphabetized parallel, piping, and indexed choices.

<div class="mw-heading mw-heading3"><h3 id="Formal_semantics">Formal semantics</h3></div>

CSP has been imbued with several different <a href="Semantics#Computer_science" title="Semantics">formal semantics</a>, which define the meaning of syntactically correct CSP expressions. The theory of CSP includes mutually consistent <a href="Denotational_semantics" title="Denotational semantics">denotational semantics</a>, <a href="Algebraic_semantics_(computer_science)" title="Algebraic semantics (computer science)">algebraic semantics</a>, and <a href="Operational_semantics" title="Operational semantics">operational semantics</a>.

<div class="mw-heading mw-heading3"><h3 id="Denotational_semantics">Denotational semantics</h3></div>

The three major denotational models of CSP are the traces model, the stable failures model, and the failures/divergences model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP.<a href="#cite_note-roscoe-1">[1]</a>

Denotational semantics allows several definitions of a <a href="Partial_order" class="mw-redirect" title="Partial order">partial order</a> of refinement on processes, which in turn can be used to elegantly represent several properties on processes. Generally, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\sqsubseteq Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\sqsubseteq Q}</annotation>

</semantics>

</math><img src="./dae230ab40c4fc12a915bd32e0b7eb6cff086ed5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.682ex; height:2.509ex;" alt="{\displaystyle P\sqsubseteq Q}" loading="lazy"> denotes <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> refines <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">.

<div class="mw-heading mw-heading4"><h4 id="Traces_model">Traces model</h4></div>

The traces model defines the meaning of a process expression as the set of sequences of events (traces) that the process can be observed to perform. For example,

</mrow>

<mrow>

</mrow>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}}</annotation>

</semantics>

</math><img src="./ca38aa540727e22409b5b7fee8903dcc88f0992a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.75ex; height:2.843ex;" alt="{\displaystyle \mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}}" loading="lazy"> since <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {STOP} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {STOP} }</annotation>

</semantics>

</math><img src="./e23c64a51333169346990cba6313d7d089153428.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.362ex; height:2.176ex;" alt="{\displaystyle \mathrm {STOP} }" loading="lazy"> performs no events</li>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}}</annotation>

</semantics>

</math><img src="./771636bd82f1333f951c76bda87dc1c8e92c53f6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:41.384ex; height:2.843ex;" alt="{\displaystyle \mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}}" loading="lazy"> since the process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (a\rightarrow b\rightarrow \mathrm {STOP} )}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (a\rightarrow b\rightarrow \mathrm {STOP} )}</annotation>

</semantics>

</math><img src="./fc994212a17013c6983e9b5966b6141293559eb7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.626ex; height:2.843ex;" alt="{\displaystyle (a\rightarrow b\rightarrow \mathrm {STOP} )}" loading="lazy"> can be observed to have performed no events, the event a, or the sequence of events a followed by b</li></ul>

More formally, the traces model <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {T}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {T}}}</annotation>

</semantics>

</math><img src="./8236d074e42310f5dc24d1d2b5b8f5981c3e87ba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.936ex; height:2.343ex;" alt="{\displaystyle {\mathcal {T}}}" loading="lazy"> is defined as the set of non-empty prefix-closed subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma ^{\ast }}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Sigma ^{\ast }}</annotation>

</semantics>

</math><img src="./494363f77d5e8c30fd81b8cb01b3c02c79d55f11.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.732ex; height:2.343ex;" alt="{\displaystyle \Sigma ^{\ast }}" loading="lazy">. The meaning of a process P in the traces model is defined as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }}">

</mrow>

<mrow>

</mrow>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }}</annotation>

</semantics>

</math><img src="./5c2194b93ddd38eb69354ebf0f5a2700a78170c9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.732ex; height:2.843ex;" alt="{\displaystyle \mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }}" loading="lazy"> such that:

</mrow>

<mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle \rangle \in \mathrm {traces} \left(P\right)}</annotation>

</semantics>

</math><img src="./4e3ec46bca6d98fba2fd2b8ce52cf5d2a153838f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.552ex; height:2.843ex;" alt="{\displaystyle \langle \rangle \in \mathrm {traces} \left(P\right)}" loading="lazy"> (i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {traces} \left(P\right)}">

</mrow>

<mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {traces} \left(P\right)}</annotation>

</semantics>

</math><img src="./5f10956576407a34aac7427b0e721d8c4f40e62e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.902ex; height:2.843ex;" alt="{\displaystyle \mathrm {traces} \left(P\right)}" loading="lazy"> contains the empty sequence)</li>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mrow>

<mrow>

</mrow>

<msub>

</mrow>

</msub>

</mrow>

<mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)}</annotation>

</semantics>

</math><img src="./15dd106d53963e71bc50ef55613ac6e094467f9a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:41.403ex; height:2.843ex;" alt="{\displaystyle s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)}" loading="lazy"> (i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {traces} \left(P\right)}">

</mrow>

<mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {traces} \left(P\right)}</annotation>

</semantics>

</math><img src="./5f10956576407a34aac7427b0e721d8c4f40e62e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.902ex; height:2.843ex;" alt="{\displaystyle \mathrm {traces} \left(P\right)}" loading="lazy"> is prefix-closed)</li></ol>

where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma ^{\ast }}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Sigma ^{\ast }}</annotation>

</semantics>

</math><img src="./494363f77d5e8c30fd81b8cb01b3c02c79d55f11.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.732ex; height:2.343ex;" alt="{\displaystyle \Sigma ^{\ast }}" loading="lazy"> is the set of all possible finite sequences of events.

A process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> is said to trace-refine another <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {traces} (P)\supseteq \mathrm {traces} (Q)}">

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {traces} (P)\supseteq \mathrm {traces} (Q)}</annotation>

</semantics>

</math><img src="./6e5e06fb7bde2e29c636a399779b8ab4179c99ef.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:22.22ex; height:2.843ex;" alt="{\displaystyle \mathrm {traces} (P)\supseteq \mathrm {traces} (Q)}" loading="lazy">. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> trace-refines <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> is denoted <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q\sqsubseteq _{\mathrm {T} }P}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q\sqsubseteq _{\mathrm {T} }P}</annotation>

</semantics>

</math><img src="./80c5fca43d2cb04fedb68cf4f0020c0e54697556.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:8.101ex; height:2.509ex;" alt="{\displaystyle Q\sqsubseteq _{\mathrm {T} }P}" loading="lazy">.<a href="#cite_note-ucs-18">[18]</a>

<div class="mw-heading mw-heading4"><h4 id="Stable_failures_model">Stable failures model</h4></div>

The stable failures model <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {F}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {F}}}</annotation>

</semantics>

</math><img src="./205d4b91000d9dcf1a5bbabdfa6a8395fa60b676.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.927ex; height:2.176ex;" alt="{\displaystyle {\mathcal {F}}}" loading="lazy"> extends the traces model with refusal sets, which are sets of events <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle X\subseteq \Sigma }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle X\subseteq \Sigma }</annotation>

</semantics>

</math><img src="./18f79703984f68d0b2044ae1309747ac56db6702.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.757ex; height:2.343ex;" alt="{\displaystyle X\subseteq \Sigma }" loading="lazy"> that a process can refuse to perform. A failure is a pair <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \left(s,X\right)}">

<mrow>

<mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \left(s,X\right)}</annotation>

</semantics>

</math><img src="./7efb29bd972755acad35086df67dabd6669ea612.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.914ex; height:2.843ex;" alt="{\displaystyle \left(s,X\right)}" loading="lazy">, consisting of a trace s, and a refusal set X which identifies the events that a process may refuse once it has executed the trace s. The observed behavior of a process in the stable failures model is described by the pair <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)}">

<mrow>

<mrow>

</mrow>

<mrow>

</mrow>

</mrow>

<mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)}</annotation>

</semantics>

</math><img src="./499a458d3c540c94bf61416db1887cbe57534a9a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.548ex; height:2.843ex;" alt="{\displaystyle \left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)}" loading="lazy">. For example,

</mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\Box \left(b\rightarrow \mathrm {STOP} \right)\right)=\left\{\left(\langle \rangle ,\emptyset \right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}}</annotation>

</semantics>

</math>

</mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\sqcap \left(b\rightarrow \mathrm {STOP} \right)\right)=\left\{\left(\langle \rangle ,\left\{a\right\}\right),\left(\langle \rangle ,\left\{b\right\}\right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}}</annotation>

</semantics>

</math>

A process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> stable-failures-refines <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {traces} (P)\supseteq \mathrm {traces} (Q)\land \mathrm {failures} (P)\supseteq \mathrm {failures} (Q)}">

</mrow>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {traces} (P)\supseteq \mathrm {traces} (Q)\land \mathrm {failures} (P)\supseteq \mathrm {failures} (Q)}</annotation>

</semantics>

</math><img src="./2a01c3e0651960046874098e46d25d36befaab3d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:50.052ex; height:2.843ex;" alt="{\displaystyle \mathrm {traces} (P)\supseteq \mathrm {traces} (Q)\land \mathrm {failures} (P)\supseteq \mathrm {failures} (Q)}" loading="lazy">. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> stable-failures-refines <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> is denoted <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q\sqsubseteq _{\mathrm {F} }P}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q\sqsubseteq _{\mathrm {F} }P}</annotation>

</semantics>

</math><img src="./c92d33f193ce082b5f31a69113111f7ea89820ef.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:7.988ex; height:2.509ex;" alt="{\displaystyle Q\sqsubseteq _{\mathrm {F} }P}" loading="lazy">.<a href="#cite_note-ucs-18">[18]</a>

<div class="mw-heading mw-heading4"><h4 id="Failures/divergences_model">Failures/divergences model</h4></div>

The failures/divergence model <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {N}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {N}}}</annotation>

</semantics>

</math><img src="./b7551c7bed2cd2ee83e10536d157c94a5f8f72fd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-left: -0.062ex; width:2.337ex; height:2.509ex;" alt="{\displaystyle {\mathcal {N}}}" loading="lazy"> further extends the failures model to handle <a href="Divergence_(computer_science)" title="Divergence (computer science)">divergence</a>. The semantics of a process in the failures/divergences model is a pair <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)}">

<mrow>

<mrow>

<msub>

</mrow>

</mrow>

</msub>

<mrow>

</mrow>

</mrow>

<mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)}</annotation>

</semantics>

</math><img src="./e58b0691e40f880d8e7b8950c199075da53ae363.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:31.678ex; height:2.843ex;" alt="{\displaystyle \left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)}" loading="lazy"> where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {divergences} \left(P\right)}">

</mrow>

<mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {divergences} \left(P\right)}</annotation>

</semantics>

</math><img src="./3b7d2cfe42bc4b1e7c8ba7a1c5e9af3f8d0806dc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.521ex; height:2.843ex;" alt="{\displaystyle \mathrm {divergences} \left(P\right)}" loading="lazy"> is defined as the extension-closure of the set of all traces after which the process can immediately diverge, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {failures} _{\perp }\left(P\right)=\mathrm {failures} \left(P\right)\cup \left\{\left(s,X\right)\mid s\in \mathrm {divergences} \left(P\right),X\subseteq \Sigma ^{*}\right\}}">

<msub>

</mrow>

</mrow>

</msub>

<mrow>

</mrow>

</mrow>

<mrow>

</mrow>

<mrow>

<mrow>

<mrow>

</mrow>

</mrow>

</mrow>

<mrow>

</mrow>

<msup>

</mrow>

</msup>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {failures} _{\perp }\left(P\right)=\mathrm {failures} \left(P\right)\cup \left\{\left(s,X\right)\mid s\in \mathrm {divergences} \left(P\right),X\subseteq \Sigma ^{*}\right\}}</annotation>

</semantics>

</math><img src="./8201e4aab47730893388fe5e2e5bbddf45e2dd4f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:68.883ex; height:2.843ex;" alt="{\displaystyle \mathrm {failures} _{\perp }\left(P\right)=\mathrm {failures} \left(P\right)\cup \left\{\left(s,X\right)\mid s\in \mathrm {divergences} \left(P\right),X\subseteq \Sigma ^{*}\right\}}" loading="lazy">, which is the extension of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {failures} (P)}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {failures} (P)}</annotation>

</semantics>

</math><img src="./2ce67d2f96304ce092fd0c7d49a0c5d6c134b143.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.029ex; height:2.843ex;" alt="{\displaystyle \mathrm {failures} (P)}" loading="lazy"> with all divergent traces.

A process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> failures-divergences-refines <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {failures} _{\bot }(P)\supseteq \mathrm {failures} _{\bot }(Q)\land \mathrm {divergences} (P)\supseteq \mathrm {divergences} (Q)}">

<msub>

</mrow>

</mrow>

</msub>

<msub>

</mrow>

</mrow>

</msub>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {failures} _{\bot }(P)\supseteq \mathrm {failures} _{\bot }(Q)\land \mathrm {divergences} (P)\supseteq \mathrm {divergences} (Q)}</annotation>

</semantics>

</math><img src="./34a187da9c390873884e492def3f98d9f81a5119.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:64.313ex; height:2.843ex;" alt="{\displaystyle \mathrm {failures} _{\bot }(P)\supseteq \mathrm {failures} _{\bot }(Q)\land \mathrm {divergences} (P)\supseteq \mathrm {divergences} (Q)}" loading="lazy">. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> failures-divergences refines <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> is denoted <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q\sqsubseteq _{\mathrm {FD} }P}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q\sqsubseteq _{\mathrm {FD} }P}</annotation>

</semantics>

</math><img src="./d8008799550a0b4094bafb5b446079b35e8807c2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:9.243ex; height:2.509ex;" alt="{\displaystyle Q\sqsubseteq _{\mathrm {FD} }P}" loading="lazy">.<a href="#cite_note-ucs-18">[18]</a>

<div class="mw-heading mw-heading4"><h4 id="Unique_fixed_points">Unique fixed points</h4></div>

One of the most important principles in CSP is the unique fixed points (UFP) rule. Generally, it states that a process which satisfies certain nice properties has a single semantic interpretation. It can be used to conclude algebraic proofs that two processes are equal in a model of CSP. A version for single recursions in the traces model is outlined here.

Consider processes as their trace sets. The operator <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \downarrow }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \downarrow }</annotation>

</semantics>

</math><img src="./4618f22b0f780805eb94bb407578d9bc9487947a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.162ex; height:2.509ex;" alt="{\displaystyle \downarrow }" loading="lazy"> is defined for all processes <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">, all <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n\in \mathbb {N} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n\in \mathbb {N} }</annotation>

</semantics>

</math><img src="./d059936e77a2d707e9ee0a1d9575a1d693ce5d0b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.913ex; height:2.176ex;" alt="{\displaystyle n\in \mathbb {N} }" loading="lazy"> so that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\downarrow n=\{s\in P:\#s\leq n\}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\downarrow n=\{s\in P:\#s\leq n\}}</annotation>

</semantics>

</math><img src="./feab0836ecd0baa9831d99ae6c69f99dc70f2f08.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:26.15ex; height:2.843ex;" alt="{\displaystyle P\downarrow n=\{s\in P:\#s\leq n\}}" loading="lazy">, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \#s}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \#s}</annotation>

</semantics>

</math><img src="./717b9fd460bb89ac0fad39f677160bd374175ed0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.026ex; height:2.509ex;" alt="{\displaystyle \#s}" loading="lazy"> denotes the length of string <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle s}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle s}</annotation>

</semantics>

</math><img src="./01d131dfd7673938b947072a13a9744fe997e632.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.09ex; height:1.676ex;" alt="{\displaystyle s}" loading="lazy">: the set of traces in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy"> of length at most <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy">. This allows a <a href="Metric_space" title="Metric space">metric</a> to be defined on <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {T}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {T}}}</annotation>

</semantics>

</math><img src="./8236d074e42310f5dc24d1d2b5b8f5981c3e87ba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.936ex; height:2.343ex;" alt="{\displaystyle {\mathcal {T}}}" loading="lazy">. For each <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy">, let <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle d(P,Q)=\mathrm {inf} \{2^{-n}:P\downarrow n=Q\downarrow n\}}">

</mrow>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle d(P,Q)=\mathrm {inf} \{2^{-n}:P\downarrow n=Q\downarrow n\}}</annotation>

</semantics>

</math><img src="./031d3fc2453c24cbfba5a7ebcde7f977c9b91780.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:35.845ex; height:3.009ex;" alt="{\displaystyle d(P,Q)=\mathrm {inf} \{2^{-n}:P\downarrow n=Q\downarrow n\}}" loading="lazy">. Informally, a process which agrees on traces with another up to some length is ‘more distant’ from it than one which agrees with it up to a greater length. It can be shown that this forms a <a href="Complete_metric_space" title="Complete metric space">complete metric space</a>.

A function on trace sets <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F:{\mathcal {T}}\rightarrow {\mathcal {T}}}">

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F:{\mathcal {T}}\rightarrow {\mathcal {T}}}</annotation>

</semantics>

</math><img src="./b84370f813c089958f210626103b348c4214cec7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:11.164ex; height:2.343ex;" alt="{\displaystyle F:{\mathcal {T}}\rightarrow {\mathcal {T}}}" loading="lazy"> is called constructive if and only if for all processes <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P}</annotation>

</semantics>

</math><img src="./b4dc73bf40314945ff376bd363916a738548d40a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy">, all <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n\in \mathbb {N} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n\in \mathbb {N} }</annotation>

</semantics>

</math><img src="./d059936e77a2d707e9ee0a1d9575a1d693ce5d0b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.913ex; height:2.176ex;" alt="{\displaystyle n\in \mathbb {N} }" loading="lazy">, if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\downarrow n=Q\downarrow n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P\downarrow n=Q\downarrow n}</annotation>

</semantics>

</math><img src="./3b339b92f00c26fca4f49fc2f77e1f70caa6a288.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:14.377ex; height:2.509ex;" alt="{\displaystyle P\downarrow n=Q\downarrow n}" loading="lazy"> then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F(P)\downarrow (n+1)=F(Q)\downarrow (n+1)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F(P)\downarrow (n+1)=F(Q)\downarrow (n+1)}</annotation>

</semantics>

</math><img src="./49a8872be5d6a7a8cc2c6e4cb7ff1d7168186f22.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.102ex; height:2.843ex;" alt="{\displaystyle F(P)\downarrow (n+1)=F(Q)\downarrow (n+1)}" loading="lazy">. This means that a function is constructive if and only if it is a <a href="Contraction_mapping" title="Contraction mapping">contraction mapping</a> with respect to the metric on trace sets.

By the <a href="Banach_fixed-point_theorem" title="Banach fixed-point theorem">Banach fixed-point theorem</a>, if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F}</annotation>

</semantics>

</math><img src="./545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"> is a constructive function, it has a unique <a href="Fixed_point_(mathematics)" title="Fixed point (mathematics)">fixed point</a>. This means that if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle X}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle X}</annotation>

</semantics>

</math><img src="./68baa052181f707c662844a465bfeeb135e82bab.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.98ex; height:2.176ex;" alt="{\displaystyle X}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Y}</annotation>

</semantics>

</math><img src="./961d67d6b454b4df2301ac571808a3538b3a6d3f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.171ex; width:1.773ex; height:2.009ex;" alt="{\displaystyle Y}" loading="lazy"> are processes defined recursively as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle X=F(X)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle X=F(X)}</annotation>

</semantics>

</math><img src="./11c9c3c5e34e71117ccb213f3341fc16b5e8c111.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.609ex; height:2.843ex;" alt="{\displaystyle X=F(X)}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Y=F(Y)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Y=F(Y)}</annotation>

</semantics>

</math><img src="./ff6715d3628a1392db3f96b9ce1081d3bf07793f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.195ex; height:2.843ex;" alt="{\displaystyle Y=F(Y)}" loading="lazy">, then they are equivalent in the traces model. UFP can also be extended to mutual recursions (by using vectors of processes) and other models of CSP (e.g. in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {F}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {F}}}</annotation>

</semantics>

</math><img src="./205d4b91000d9dcf1a5bbabdfa6a8395fa60b676.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.927ex; height:2.176ex;" alt="{\displaystyle {\mathcal {F}}}" loading="lazy"> by defining the metric as in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {T}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {T}}}</annotation>

</semantics>

</math><img src="./8236d074e42310f5dc24d1d2b5b8f5981c3e87ba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.936ex; height:2.343ex;" alt="{\displaystyle {\mathcal {T}}}" loading="lazy">, with respect to the trace parts of a process's trace-failure pair).

It can be derived using UFP (and <a href="Tarski's_fixed_point_theorem" class="mw-redirect" title="Tarski's fixed point theorem">Tarski's fixed point theorem</a>), that for <a href="Monotonic_function" title="Monotonic function">monotonic</a> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F}</annotation>

</semantics>

</math><img src="./545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy">, a recursive term defined as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle X=F(X)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle X=F(X)}</annotation>

</semantics>

</math><img src="./11c9c3c5e34e71117ccb213f3341fc16b5e8c111.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.609ex; height:2.843ex;" alt="{\displaystyle X=F(X)}" loading="lazy"> has the semantic interpretation <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \sqcap _{n=0}^{\infty }F^{n}(\bot )}">

</mrow>

</mrow>

</msubsup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \sqcap _{n=0}^{\infty }F^{n}(\bot )}</annotation>

</semantics>

</math><img src="./2b842d3680665bb3fbaaba4ec5b3cb58e97c1ed5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:11.52ex; height:3.009ex;" alt="{\displaystyle \sqcap _{n=0}^{\infty }F^{n}(\bot )}" loading="lazy">, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bot }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bot }</annotation>

</semantics>

</math><img src="./f282c7bc331cc3bfcf1c57f1452cc23c022f58de.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \bot }" loading="lazy"> is the least element of the model. In the traces, stable failures and failures/divergences models, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bot =\mathbf {div} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bot =\mathbf {div} }</annotation>

</semantics>

</math><img src="./cc4866bab2a6223ec30f103c31165d0c272c9b59.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:8.545ex; height:2.176ex;" alt="{\displaystyle \bot =\mathbf {div} }" loading="lazy"> (equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathrm {STOP} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {STOP} }</annotation>

</semantics>

</math><img src="./e23c64a51333169346990cba6313d7d089153428.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.362ex; height:2.176ex;" alt="{\displaystyle \mathrm {STOP} }" loading="lazy"> in the traces model).<a href="#cite_note-roscoe-1">[1]</a><a href="#cite_note-ucs-18">[18]</a>

<div class="mw-heading mw-heading2"><h2 id="Tools">Tools</h2></div>

Over the years, a number of tools for analyzing and understanding systems described using CSP have been produced. Early tool implementations used a variety of machine-readable syntaxes for CSP, making input files written for different tools incompatible. However, most CSP tools have now standardized on the machine-readable dialect of CSP devised by Bryan Scattergood, sometimes referred to as CSPM.<a href="#cite_note-19">[19]</a> The CSPM dialect of CSP possesses a formally defined <a href="Operational_semantics" title="Operational semantics">operational semantics</a>, which includes an embedded <a href="Functional_programming_language" class="mw-redirect" title="Functional programming language">functional programming language</a>.

The most well-known CSP tool is probably <a href="FDR_(software)" title="FDR (software)">Failures-Divergences Refinement</a>, which is a commercial product originally developed by Formal Systems (Europe) Ltd. FDR is often described as a <a href="Model_checker" class="mw-redirect" title="Model checker">model checker</a>, but is technically a refinement checker, in that it converts two CSP process expressions into <a href="Labelled_transition_system" class="mw-redirect" title="Labelled transition system">labelled transition systems</a> (LTSs), and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, or failures/divergence).<a href="#cite_note-20">[20]</a> FDR applies various state-space compression algorithms to the process LTSs in order to reduce the size of the state-space that must be explored during a refinement check. FDR was succeeded by FDR2, FDR3 and FDR4.<a href="#cite_note-21">[21]</a>

The Adelaide Refinement Checker (ARC)<a href="#cite_note-22">[22]</a> is a CSP refinement checker developed by the Formal Modelling and Verification Group at <a href="The_University_of_Adelaide" class="mw-redirect" title="The University of Adelaide">The University of Adelaide</a>. ARC differs from FDR2 in that it internally represents CSP processes as ordered <a href="Binary_decision_diagram" title="Binary decision diagram">binary decision diagrams</a> (OBDDs), which alleviates the state explosion problem of explicit LTS representations without requiring the use of state-space compression algorithms such as those used in FDR2.

The ProB project,<a href="#cite_note-23">[23]</a> which is hosted by the Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, was originally created to support analysis of specifications constructed in the <a href="B_method" class="mw-redirect" title="B method">B method</a>. However, it also includes support for analysis of CSP processes both through refinement checking, and <a href="Linear_Temporal_Logic" class="mw-redirect" title="Linear Temporal Logic">LTL</a> model-checking. ProB can also be used to verify properties of combined CSP and B specifications. A ProBE CSP Animator is integrated in FDR3.

The Process Analysis Toolkit (PAT)

<a href="#cite_note-24">[24]</a><a href="#cite_note-25">[25]</a> is a CSP analysis tool developed in the School of Computing at the <a href="National_University_of_Singapore" title="National University of Singapore">National University of Singapore</a>. PAT is able to perform refinement checking, LTL model-checking, and simulation of CSP and Timed CSP processes. The PAT process language extends CSP with support for mutable shared variables, asynchronous message passing, and a variety of fairness and quantitative time related process constructs such as <code>deadline</code> and <code>waituntil</code>. The underlying design principle of the PAT process language is to combine a high-level specification language with procedural programs (e.g. an event in PAT may be a sequential program or even an external C# library call) for greater expressiveness. Mutable shared variables and asynchronous channels provide a convenient <a href="Syntactic_sugar" title="Syntactic sugar">syntactic sugar</a> for well-known process modelling patterns used in standard CSP. The PAT syntax is similar, but not identical, to CSPM.<a href="#cite_note-26">[26]</a> The principal differences between the PAT syntax and standard CSPM are the use of semicolons to terminate process expressions, the inclusion of syntactic sugar for variables and assignments, and the use of slightly different syntax for internal choice and parallel composition.

<div class="mw-heading mw-heading3"><h3 id="Others">Others</h3></div>

VisualNets<a href="#cite_note-27">[27]</a> produces animated visualisations of CSP systems from specifications, and supports timed CSP.

CSPsim<a href="#cite_note-28">[28]</a> is a lazy simulator. It does not model check CSP, but is useful for exploring very large (potentially infinite) systems.

<a rel="nofollow" class="external text" href="http://www.principia-m.com/syncstitch/">SyncStitch</a> is a CSP refinement checker with interactive modeling and analyzing environment. It has a graphical state-transition diagram editor. The user can model the behavior of processes as not only CSP expressions but also state-transition diagrams. The result of checking are also reported graphically as computation-trees and can be analyzed interactively with peripheral inspecting tools. In addition to refinement checks, It can perform deadlock check and livelock check.

<div class="mw-heading mw-heading2"><h2 id="Related_formalisms">Related formalisms</h2></div>

Several other specification languages and formalisms have been derived from, or inspired by, the classic untimed CSP, including:

<ul><li><a rel="nofollow" class="external text" href="https://www.sciencedirect.com/science/article/pii/S1571066106004464/pdf">Timed CSP</a>, which incorporates timing information for reasoning about real-time systems</li>

<li><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1007/BF01178564">Receptive Process Theory</a>, a specialization of CSP that assumes an asynchronous (i.e. <a href="Non-blocking_algorithm" title="Non-blocking algorithm">nonblocking</a>) send operation</li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20110514234220/http://www.comp.nus.edu.sg/~dongjs/tcoz.html">TCOZ</a>, an integration of Timed CSP and <a href="Object_Z" class="mw-redirect" title="Object Z">Object Z</a></li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/">Circus</a>, an integration of CSP and <a href="Z_specification_language" class="mw-redirect" title="Z specification language">Z</a> based on the <a href="Unifying_Theories_of_Programming" title="Unifying Theories of Programming">Unifying Theories of Programming</a></li>

<li><a rel="nofollow" class="external text" href="http://www.compass-research.eu/approach.html">CML</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20200219205126/http://www.compass-research.eu/approach.html">Archived</a> 2020-02-19 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a> (COMPASS Modelling Language), a combination of <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/">Circus</a> and <a href="VDM_specification_language" class="mw-redirect" title="VDM specification language">VDM</a> developed for the modelling of <a href="System_of_systems" title="System of systems">Systems of Systems</a> (SoS)</li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20110514234221/http://www.cs.swan.ac.uk/~csmarkus/Papers/cspcasl.ps">CspCASL</a>, an extension of <a href="Common_Algebraic_Specification_Language" title="Common Algebraic Specification Language">CASL</a> that integrates CSP</li>

<li><a href="Language_Of_Temporal_Ordering_Specification" class="mw-redirect" title="Language Of Temporal Ordering Specification">LOTOS</a>, an international standard<a href="#cite_note-29">[29]</a> that incorporates features of CSP and <a href="Calculus_of_Communicating_Systems" class="mw-redirect" title="Calculus of Communicating Systems">CCS</a>.</li>

<li><a rel="nofollow" class="external text" href="https://link.springer.com/chapter/10.1007/978-3-319-05032-4_25">PALPS</a>, a probabilistic extension with locations for ecological models developed by Anna Philippou and Mauricio Toro Bermúdez</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Comparison_with_the_actor_model">Comparison with the actor model</h2></div>

In as much as it is concerned with concurrent processes that exchange messages, the <a href="Actor_model" title="Actor model">actor model</a> is broadly similar to CSP. However, the two models make some fundamentally different choices with regard to the primitives they provide:

<ul><li>CSP processes are anonymous, while actors have identities.</li>

<li>CSP uses explicit channels for message passing, whereas actor systems transmit messages to named destination actors. These approaches may be considered duals of each other, in the sense that processes receiving through a single channel effectively have an identity corresponding to that channel, while the name-based coupling between actors may be broken by constructing actors that behave as channels.</li>

<li>CSP message-passing fundamentally involves a rendezvous between the processes involved in sending and receiving the message, i.e. the sender cannot transmit a message until the receiver is ready to accept it. In contrast, message-passing in actor systems is fundamentally asynchronous, i.e. message transmission and reception do not have to happen at the same time, and senders may transmit messages before receivers are ready to accept them. These approaches may also be considered duals of each other, in the sense that rendezvous-based systems can be used to construct buffered communications that behave as asynchronous messaging systems, while asynchronous systems can be used to construct rendezvous-style communications by using a message/acknowledgement protocol to synchronize senders and receivers.</li></ul>

Note that the aforementioned properties do not necessarily refer to the original CSP paper by Hoare, but rather the modern incarnation of the idea as seen in implementations such as Go and Clojure's core.async. In the original paper, channels were not a central part of the specification, and the sender and receiver processes actually identify each other by name.

<div class="mw-heading mw-heading2"><h2 id="Award">Award</h2></div>

In 1990, “A <a href="Elizabeth_II" title="Elizabeth II">Queen</a>’s Award for Technological Achievement [was] conferred ... on <a href="Oxford_University_Computing_Laboratory" class="mw-redirect" title="Oxford University Computing Laboratory">[Oxford University] Computing Laboratory</a>. The award recognises a successful collaboration between the laboratory and <a href="Inmos" title="Inmos">Inmos</a> Ltd. … Inmos’ flagship product is the ‘<a href="Transputer" title="Transputer">transputer</a>’, a <a href="Microprocessor" title="Microprocessor">microprocessor</a> with many of the parts that would normally be needed in addition built into the same single <a href="Electronic_component" title="Electronic component">component</a>.”<a href="#cite_note-30">[30]</a>

According to Tony Hoare,<a href="#cite_note-31">[31]</a>

“The INMOS Transputer was as embodiment of the ideas … of building microprocessors that could communicate with each other along wires that would stretch between their terminals. The founder had the vision that the CSP ideas were ripe for industrial exploitation, and he made that the basis of the language for programming Transputers, which was called <a href="Occam_(programming_language)" title="Occam (programming language)">Occam</a>. … The company estimated it enabled them to deliver the hardware one year earlier than would otherwise have happened. They applied for and won a Queen’s award for technological achievement, in conjunction with Oxford University Computing Laboratory.”

<ul><li><a href="Trace_theory" title="Trace theory">Trace theory</a>, the general theory of traces.</li>

<li><a href="Trace_monoid" title="Trace monoid">Trace monoid</a> and <a href="History_monoid" title="History monoid">history monoid</a></li>

<li><a href="Ease_programming_language" class="mw-redirect" title="Ease programming language">Ease programming language</a></li>

<li><a href="XC_programming_language" class="mw-redirect" title="XC programming language">XC programming language</a></li>

<li><a href="VerilogCSP" title="VerilogCSP">VerilogCSP</a> is a set of <a href="Macro_(computer_science)" title="Macro (computer science)">macros</a> added to <a href="Verilog_HDL" class="mw-redirect" title="Verilog HDL">Verilog HDL</a> to support communicating sequential processes channel communications.</li>

<li><a href="Joyce_(programming_language)" title="Joyce (programming language)">Joyce</a> is a programming language based on the principles of CSP, developed by <a href="Brinch_Hansen" class="mw-redirect" title="Brinch Hansen">Brinch Hansen</a> around 1989.</li>

<li><a href="SuperPascal" title="SuperPascal">SuperPascal</a> is a programming language also developed by <a href="Brinch_Hansen" class="mw-redirect" title="Brinch Hansen">Brinch Hansen</a>, influenced by CSP and his earlier work with <a href="Joyce_(programming_language)" title="Joyce (programming language)">Joyce</a>.</li>

<li><a href="Ada_(programming_language)" title="Ada (programming language)">Ada</a> implements features of CSP such as the rendezvous.</li>

<li><a href="DirectShow" title="DirectShow">DirectShow</a> is the video framework inside <a href="DirectX" title="DirectX">DirectX</a>, it uses the CSP concepts to implement the audio and video filters.</li>

<li><a href="OpenComRTOS" title="OpenComRTOS">OpenComRTOS</a> is a formally developed network-centric distributed <a href="RTOS" class="mw-redirect" title="RTOS">RTOS</a> based on a pragmatic superset of CSP.</li>

<li><a href="Input/output_automaton" title="Input/output automaton">Input/output automaton</a></li>

<li><a href="Parallel_programming_model" title="Parallel programming model">Parallel programming model</a></li>

<li><a href="TLA%2B" title="TLA+">TLA+</a> is another formal language for modelling and verifying concurrent systems.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist reflist-columns references-column-width reflist-columns-2">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFRoscoe1997" class="citation book cs1"><a href="Bill_Roscoe" title="Bill Roscoe">Roscoe, A. W.</a> (1997). <a rel="nofollow" class="external text" href="http://www.cs.ox.ac.uk/bill.roscoe/publications/68b.pdf">The Theory and Practice of Concurrency</a> (PDF). <a href="Prentice_Hall" title="Prentice Hall">Prentice Hall</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-13-674409-2</bdi>.</cite>

</li>

<li id="cite_note-2"><a href="#cite_ref-2">^</a> <cite id="CITEREFInmos1995" class="citation book cs1"><a href="Inmos" title="Inmos">Inmos</a> (1995-05-12). <a rel="nofollow" class="external text" href="http://www.wotug.org/occam/documentation/oc21refman.pdf">occam 2.1 Reference Manual</a> (PDF). SGS-Thomson Microelectronics Ltd.</cite>, INMOS document 72 occ 45 03.

</li>

<li id="cite_note-cox-3">^ <a href="#cite_ref-cox_3-0">a</a> <a href="#cite_ref-cox_3-1">b</a> <cite id="CITEREFCox" class="citation web cs1">Cox, Russ. <a rel="nofollow" class="external text" href="http://swtch.com/~rsc/thread/">"Bell Labs and CSP Threads"</a>. Retrieved 2010-04-15.</cite>

</li>

<li id="cite_note-4"><a href="#cite_ref-4">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://www.erlang.org/faq/academic.html">"10 Academic and Historical Questions"</a>. Retrieved 2021-11-15.</cite>

</li>

<li id="cite_note-golang-5"><a href="#cite_ref-golang_5-0">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://golang.org/doc/go_faq.html#csp">"FAQ: Why build concurrency on the ideas of CSP?"</a>. The Go Programming Language. Retrieved 2021-10-15.</cite>

</li>

<li id="cite_note-clojure-core-async-6"><a href="#cite_ref-clojure-core-async_6-0">^</a> <cite id="CITEREFHickey2013" class="citation web cs1">Hickey, Rich (2013-06-28). <a rel="nofollow" class="external text" href="https://clojure.org/news/2013/06/28/clojure-clore-async-channels#_history">"Clojure core.async Channels"</a>. Retrieved 2021-10-15.</cite>

</li>

<li id="cite_note-hoare1978-7">^ <a href="#cite_ref-hoare1978_7-0">a</a> <a href="#cite_ref-hoare1978_7-1">b</a> <cite id="CITEREFHoare1978" class="citation journal cs1"><a href="C._A._R._Hoare" class="mw-redirect" title="C. A. R. Hoare">Hoare, C. A. R.</a> (1978). <a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F359576.359585">"Communicating sequential processes"</a>. <a href="Communications_of_the_ACM" title="Communications of the ACM">Communications of the ACM</a>. 21 (8): 666–677. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F359576.359585">10.1145/359576.359585</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:849342">849342</a>.</cite>

</li>

<li id="cite_note-25years-8"><a href="#cite_ref-25years_8-0">^</a> <cite id="CITEREFAbdallahJonesSanders2005" class="citation book cs1">Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). <a rel="nofollow" class="external text" href="https://www.springer.com/computer/theoretical+computer+science/foundations+of+computations/book/978-3-540-25813-1">Communicating Sequential Processes: The First 25 Years</a>. <a href="LNCS" class="mw-redirect" title="LNCS">LNCS</a>. Vol. 3525. Springer. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9783540258131</bdi>.</cite>

</li>

<li id="cite_note-barrett-9">^ <a href="#cite_ref-barrett_9-0">a</a> <a href="#cite_ref-barrett_9-1">b</a> <cite id="CITEREFBarrett1995" class="citation journal cs1">Barrett, G. (1995). "Model checking in practice: The T9000 Virtual Channel Processor". IEEE Transactions on Software Engineering. 21 (2): 69–78. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2F32.345823">10.1109/32.345823</a>.</cite>

</li>

<li id="cite_note-hall-10">^ <a href="#cite_ref-hall_10-0">a</a> <a href="#cite_ref-hall_10-1">b</a> <cite id="CITEREFHallChapman2002" class="citation journal cs1">Hall, A; Chapman, R. (2002). <a rel="nofollow" class="external text" href="http://www.anthonyhall.org/c_by_c_secure_system.pdf">"Correctness by construction: Developing a commercial secure system"</a> (PDF). IEEE Software. 19 (1): 18–25. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.1811">10.1.1.16.1811</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2F52.976937">10.1109/52.976937</a>.</cite>

</li>

<li id="cite_note-11"><a href="#cite_ref-11">^</a> <cite id="CITEREFCreese2001" class="citation thesis cs1">Creese, S. (2001). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks (D. Phil.). <a href="Oxford_University" class="mw-redirect" title="Oxford University">Oxford University</a>. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.7185">10.1.1.13.7185</a>.</cite>

</li>

<li id="cite_note-hoare-12">^ <a href="#cite_ref-hoare_12-0">a</a> <a href="#cite_ref-hoare_12-1">b</a> <cite id="CITEREFHoare1985" class="citation book cs1"><a href="C._A._R._Hoare" class="mw-redirect" title="C. A. R. Hoare">Hoare, C. A. R.</a> (1985). Communicating Sequential Processes. Prentice Hall. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-13-153289-2</bdi>.</cite>

</li>

<li id="cite_note-clinger1981-13"><a href="#cite_ref-clinger1981_13-0">^</a> <cite id="CITEREFClinger1981" class="citation thesis cs1"><a href="William_Clinger_(computer_scientist)" title="William Clinger (computer scientist)">Clinger, William</a> (June 1981). Foundations of Actor Semantics (Mathematics Doctoral Dissertation). MIT. <a href="Hdl_(identifier)" class="mw-redirect" title="Hdl (identifier)">hdl</a>:<a rel="nofollow" class="external text" href="https://hdl.handle.net/1721.1%2F6935">1721.1/6935</a>.</cite>

</li>

<li id="cite_note-14"><a href="#cite_ref-14">^</a> <cite id="CITEREFBrookesHoareRoscoe1984" class="citation journal cs1">Brookes, Stephen; <a href="C._A._R._Hoare" class="mw-redirect" title="C. A. R. Hoare">Hoare, C. A. R.</a>; <a href="Bill_Roscoe" title="Bill Roscoe">Roscoe, A. W.</a> (1984). <a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F828.833">"A Theory of Communicating Sequential Processes"</a>. <a href="Journal_of_the_ACM" title="Journal of the ACM">Journal of the ACM</a>. 31 (3): 560–599. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F828.833">10.1145/828.833</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:488666">488666</a>.</cite>

</li>

<li id="cite_note-15"><a href="#cite_ref-15">^</a> <cite id="CITEREFButhM._KouvarasJ._PeleskaH._Shi1997" class="citation conference cs1">Buth, B.; M. Kouvaras; J. Peleska; H. Shi (December 1997). "Deadlock analysis for a fault-tolerant system". Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97). pp. 60–75.</cite>

</li>

<li id="cite_note-16"><a href="#cite_ref-16">^</a> <cite id="CITEREFButhJ._PeleskaH._Shi1999" class="citation conference cs1">Buth, B.; J. Peleska; H. Shi (January 1999). "Combining methods for the livelock analysis of a fault-tolerant system". Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98). pp. 124–139.</cite>

</li>

<li id="cite_note-17"><a href="#cite_ref-17">^</a> <cite id="CITEREFLowe1996" class="citation conference cs1">Lowe, G. (1996). <a rel="nofollow" class="external text" href="http://citeseer.ist.psu.edu/lowe96breaking.html">"Breaking and fixing the Needham–Schroeder public-key protocol using FDR"</a>. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag. pp. 147–166.</cite>

</li>

<li id="cite_note-ucs-18">^ <a href="#cite_ref-ucs_18-0">a</a> <a href="#cite_ref-ucs_18-1">b</a> <a href="#cite_ref-ucs_18-2">c</a> <a href="#cite_ref-ucs_18-3">d</a> <a href="#cite_ref-ucs_18-4">e</a> <a href="#cite_ref-ucs_18-5">f</a> <a href="#cite_ref-ucs_18-6">g</a> <a href="#cite_ref-ucs_18-7">h</a> <a href="#cite_ref-ucs_18-8">i</a> <a href="#cite_ref-ucs_18-9">j</a> <a href="#cite_ref-ucs_18-10">k</a> <a href="#cite_ref-ucs_18-11">l</a> <a href="#cite_ref-ucs_18-12">m</a> <cite id="CITEREFRoscoe2010" class="citation book cs1">Roscoe, A.W. (2010). Understanding Concurrent Systems. Texts in Computer Science. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-1-84882-258-0">10.1007/978-1-84882-258-0</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-84882-257-3</bdi>.</cite>

</li>

<li id="cite_note-19"><a href="#cite_ref-19">^</a> <cite id="CITEREFScattergood1998" class="citation thesis cs1">Scattergood, J. B. (1998). The Semantics and Implementation of Machine-Readable CSP (<a href="D.Phil." class="mw-redirect" title="D.Phil.">D.Phil.</a>). <a href="Oxford_University_Computing_Laboratory" class="mw-redirect" title="Oxford University Computing Laboratory">Oxford University Computing Laboratory</a>.</cite>

</li>

<li id="cite_note-20"><a href="#cite_ref-20">^</a> <cite id="CITEREFRoscoe1994" class="citation book cs1"><a href="Bill_Roscoe" title="Bill Roscoe">Roscoe, A. W.</a> (1994). "Model-checking CSP". A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice Hall.</cite>

</li>

<li id="cite_note-21"><a href="#cite_ref-21">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://www.cs.ox.ac.uk/projects/fdr/manual/introduction.html">"Introduction — FDR 4.2.4 documentation"</a>. www.cs.ox.ac.uk.</cite>

</li>

<li id="cite_note-22"><a href="#cite_ref-22">^</a> <cite id="CITEREFParashkevovYantchev1996" class="citation conference cs1">Parashkevov, Atanas N.; Yantchev, Jay (1996). "ARC – a tool for efficient refinement and equivalence checking for CSP". IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96. pp. 68–75. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.3212">10.1.1.45.3212</a>.</cite>

</li>

<li id="cite_note-23"><a href="#cite_ref-23">^</a> <cite id="CITEREFLeuschelFontaine2008" class="citation conference cs1">Leuschel, Michael; Fontaine, Marc (2008). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110719102153/http://www.stups.uni-duesseldorf.de/publications/main.pdf">"Probing the Depths of CSP-M: A new FDR-compliant Validation Tool"</a> (PDF). ICFEM 2008. Springer-Verlag. Archived from <a rel="nofollow" class="external text" href="http://www.stups.uni-duesseldorf.de/publications/main.pdf">the original</a> (PDF) on 2011-07-19. Retrieved 2008-11-26.</cite>

</li>

<li id="cite_note-24"><a href="#cite_ref-24">^</a> <cite id="CITEREFSunLiuDong2009" class="citation conference cs1">Sun, Jun; Liu, Yang; Dong, Jin Song (2009). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110611055744/http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf">"PAT: Towards Flexible Verification under Fairness"</a> (PDF). Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009). Lecture Notes in Computer Science. Vol. 5643. Springer. Archived from <a rel="nofollow" class="external text" href="http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf">the original</a> (PDF) on 2011-06-11. Retrieved 2009-06-16.</cite>

</li>

<li id="cite_note-25"><a href="#cite_ref-25">^</a> <cite id="CITEREFSunLiuDong2008" class="citation conference cs1">Sun, Jun; Liu, Yang; Dong, Jin Song (2008). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20090108091954/http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf">"Model Checking CSP Revisited: Introducing a Process Analysis Toolkit"</a> (PDF). Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008). Communications in Computer and Information Science. Vol. 17. Springer. pp. 307–322. Archived from <a rel="nofollow" class="external text" href="http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf">the original</a> (PDF) on 2009-01-08. Retrieved 2009-01-15.</cite>

</li>

<li id="cite_note-26"><a href="#cite_ref-26">^</a> <cite id="CITEREFSunLiuDongChen2009" class="citation conference cs1">Sun, Jun; Liu, Yang; Dong, Jin Song; Chen, Chunqing (2009). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110611055219/http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf">"Integrating Specifications and Programs for System Specification and Verification"</a> (PDF). IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09. Archived from <a rel="nofollow" class="external text" href="http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf">the original</a> (PDF) on 2011-06-11. Retrieved 2009-04-13.</cite>

</li>

<li id="cite_note-27"><a href="#cite_ref-27">^</a> <cite id="CITEREFGreenAbdallah2002" class="citation conference cs1">Green, Mark; Abdallah, Ali (2002). <a rel="nofollow" class="external text" href="https://www.researchgate.net/publication/290383042">"Performance Analysis and Behaviour Tuning for Optimisation of Communicating Systems"</a>. Communicating Process Architectures 2002.</cite>

</li>

<li id="cite_note-28"><a href="#cite_ref-28">^</a> <cite id="CITEREFBrookePaige2007" class="citation conference cs1">Brooke, Phillip; Paige, Richard (2007). "Lazy Exploration and Checking of CSP Models with CSPsim". Communicating Process Architectures 2007.</cite>

</li>

<li id="cite_note-29"><a href="#cite_ref-29">^</a> <a href="Language_Of_Temporal_Ordering_Specification" class="mw-redirect" title="Language Of Temporal Ordering Specification">ISO 8807, Language of Temporal Ordering Specification</a>

</li>

<li id="cite_note-30"><a href="#cite_ref-30">^</a> <cite id="CITEREFGeraint_Jones1990" class="citation journal cs1"><a href="Geraint_Jones" title="Geraint Jones">Geraint Jones</a> (1990). <a rel="nofollow" class="external text" href="http://www.cs.ox.ac.uk/people/geraint.jones/ftp/pub/Documents/techpapers/Geraint.Jones/QATA-1-90.ps">"Sharp as a Razor: A Queen's Award for the Computing Laboratory"</a>. <a href="The_Oxford_Magazine" title="The Oxford Magazine">The Oxford Magazine</a> (59, Fourth Week, Trinity Term).</cite>

</li>

<li id="cite_note-31"><a href="#cite_ref-31">^</a> <cite id="CITEREFLen_Shustek2009" class="citation journal cs1">Len Shustek (March 2009). <a rel="nofollow" class="external text" href="https://dl.acm.org/doi/abs/10.1145/1467247.1467261">"An interview with C.A.R. Hoare"</a>. <a href="Communications_of_the_ACM" title="Communications of the ACM">Communications of the ACM</a>. 52 (3): 38–41. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F1467247.1467261">10.1145/1467247.1467261</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:1868477">1868477</a>.</cite>

</li>

</ol></div>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

<ul><li><cite id="CITEREFHoare2004" class="citation book cs1"><a href="C._A._R._Hoare" class="mw-redirect" title="C. A. R. Hoare">Hoare, C. A. R.</a> (2004) [1985]. <a rel="nofollow" class="external text" href="http://www.usingcsp.com/">Communicating Sequential Processes</a>. Prentice Hall International. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-13-153271-7</bdi>.</cite>

<ul><li>This book has been updated by <a href="Jim_Davies_(computer_scientist)" title="Jim Davies (computer scientist)">Jim Davies</a> at the <a href="Oxford_University_Computing_Laboratory" class="mw-redirect" title="Oxford University Computing Laboratory">Oxford University Computing Laboratory</a> and the new edition is available for download as a PDF file at the <a rel="nofollow" class="external text" href="http://www.usingcsp.com/">Using CSP</a> website.</li></ul></li>

<li><cite id="CITEREFRoscoe1997" class="citation book cs1"><a href="Bill_Roscoe" title="Bill Roscoe">Roscoe, A. W.</a> (1997). <a rel="nofollow" class="external text" href="https://archive.org/details/theorypracticeof00rosc">The Theory and Practice of Concurrency</a>. <a href="Prentice_Hall" title="Prentice Hall">Prentice Hall</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-13-674409-2</bdi>.</cite>

<ul><li>Some links relating to this book are available <a rel="nofollow" class="external text" href="http://web.comlab.ox.ac.uk/oucl/publications/books/concurrency/">here</a>. The full text is available for download as a <a rel="nofollow" class="external text" href="http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.ps">PS</a> or <a rel="nofollow" class="external text" href="http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf">PDF</a> file from Bill Roscoe's <a rel="nofollow" class="external text" href="http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/pubs.html">list</a> of academic publications.</li></ul></li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.usingcsp.com/">A PDF version of Hoare's CSP book</a> – copyright restriction apply, see the page text before downloading.</li>

<li><a rel="nofollow" class="external text" href="https://github.com/complex-system/Communicating-Sequential-Processes">The Annotation of CSP (Chinese version)</a>, non-profit translation and annotation work based on Prentice-Hall book (1985), Chaochen Zhou's Chinese version (1988), and Jim Davies's online version (2015).</li>

<li><a rel="nofollow" class="external text" href="http://www.wotug.org/">WoTUG</a>, a user group for CSP and occam style systems, contains some information about CSP and useful links.</li>

<li><a rel="nofollow" class="external text" href="http://citeseerx.ist.psu.edu/search?q=communicating+sequential+processes&submit=Search&sort=rlv&t=doc">"CSP Citations" from CiteSeer</a></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Concurrent_computing233" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Concurrent_computing233" style="font-size:114%;margin:0 4em"><a href="Concurrent_computing" title="Concurrent computing">Concurrent computing</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">General</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Concurrency_(computer_science)" title="Concurrency (computer science)">Concurrency</a></li>

<li><a href="Concurrency_control" title="Concurrency control">Concurrency control</a></li>

<li><a href="Concurrent_data_structure" title="Concurrent data structure">Concurrent data structures</a>

<ul><li><a href="Concurrent_hash_table" title="Concurrent hash table">Concurrent hash tables</a></li></ul></li>

<li><a href="Concurrent_user" title="Concurrent user">Concurrent users</a></li>

<li><a href="Indeterminacy_in_concurrent_computation" title="Indeterminacy in concurrent computation">Indeterminacy</a></li>

<li><a href="Linearizability" title="Linearizability">Linearizability</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Process_calculus" title="Process calculus">Process calculi</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul>

<li><a href="Language_Of_Temporal_Ordering_Specification" class="mw-redirect" title="Language Of Temporal Ordering Specification">LOTOS</a></li>

<li><a href="%CE%A0-calculus" title="Π-calculus">π-calculus</a></li>

<li><a href="Ambient_calculus" title="Ambient calculus">Ambient calculus</a></li>

<li><a href="API-Calculus" title="API-Calculus">API-Calculus</a></li>

<li><a href="Join-calculus" title="Join-calculus">Join-calculus</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Classic problems</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="ABA_problem" title="ABA problem">ABA problem</a></li>

<li><a href="Cigarette_smokers_problem" title="Cigarette smokers problem">Cigarette smokers problem</a></li>

<li><a href="Deadlock_(computer_science)" title="Deadlock (computer science)">Deadlock</a></li>

<li><a href="Dining_philosophers_problem" title="Dining philosophers problem">Dining philosophers problem</a></li>

<li><a href="Producer%E2%80%93consumer_problem" title="Producer–consumer problem">Producer–consumer problem</a></li>

<li><a href="Race_condition" title="Race condition">Race condition</a></li>

<li><a href="Readers%E2%80%93writers_problem" title="Readers–writers problem">Readers–writers problem</a></li>

<li><a href="Sleeping_barber_problem" title="Sleeping barber problem">Sleeping barber problem</a></li></ul>

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div>

<ul><li> Category: Concurrent computing</li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-06-30" href="https://en.wikipedia.org/wiki/?title=Communicating_sequential_processes&oldid=1298111819">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>